|``````````````````````````````````````````````````````````````````````````````|
| This file is part of the Mist compiler.                                      |
|                                                                              |
| Copyright (C) 2009 The Mist project                                          |
|                                                                              |
| For a list of contributors, see the COMMITTERS file.                         |
|                                                                              |
| The Mist compiler is free software: you can redistribute it and/or modify it |
| under the terms of the  GNU General Public License  as published by the Free |
| Software Foundation,  either version 3  of the License,  or (at your option) |
| any later version.                                                           |
|                                                                              |
| The Mist compiler  is distributed  in the hope  that it will  be useful, but |
| WITHOUT ANY WARRANTY;  without even the implied  warranty of MERCHANTABILITY |
| or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for |
| more details.                                                                |
|                                                                              |
| You should  have received a  copy of the  GNU General  Public License in the |
| COPYING file. If not, see <http://www.gnu.org/licenses/>.                    |
|______________________________________________________________________________|
|                                                                              |
| As a special exception,  you may create a  larger work that contains part or |
| all of  this input  source-file  and  distribute  that work  under  terms of |
| your choice,  so long as that work  isn't itself a compiler  using this file |
| or a modified  version thereof  as a file to  be combined with  the compiler |
| input.  Alternatively,  if  you  modify  or  redistribute  this  source-file |
| itself, you may  (at your option) remove this  special exception, which will |
| cause this file to be licensed under  the GNU General Public License without |
| this special exception.                                                      |
|______________________________________________________________________________|

type int cpp "int" KeY "int";

type bool cpp "bool" KeY "boolean";

| a <==> b
|
bool logical_equal(bool a, bool b) {
	cpp "return (a == b);";
} KeY "(a <-> b)"

| a <== b
|
bool implied(bool a, bool b) {
	cpp "return (!b || a);";
} KeY "(b -> a)"

| a ==> b
|
bool implies(bool a, bool b) {
	cpp "return (!a || b);";
} KeY "(a -> b)"

| a or b
|
bool disjunct(bool a, bool b) {
	cpp "return (a || b);";
} KeY "(a | b)"

| a and b
|
bool conjunct(bool a, bool b) {
	cpp "return (a && b);";
} KeY "(a & b)"

| a <>= b
|
bool comparable(int a, int b) {
	cpp "return true;";
} KeY "(true)"

| a <>= b
|
bool comparable(bool a, bool b) {
	cpp "return (a == b);";
} KeY "(a <-> b)"

| a <= b
|
bool smaller_equal(int a, int b) {
	cpp "return (a <= b);";
} KeY "(a <= b)"

| a <= b
|
bool smaller_equal(bool a, bool b) {
	cpp "return (a == b);";
} KeY "(a <-> b)"

| a <> b
|
bool inequal(int a, int b) {
	cpp "return (a != b);";
} KeY "(a != b)"

| a <> b
|
bool inequal(bool a, bool b) {
	cpp "return false;";
} KeY "(false)"

| a >= b
|
bool greater_equal(int a, int b) {
	cpp "return (a >= b);";
} KeY "(a >= b)"

| a >= b
|
bool greater_equal(bool a, bool b) {
	cpp "return (a == b);";
} KeY "(a <-> b)"

| a < b
|
bool smaller(int a, int b) {
	cpp "return (a < b);";
} KeY "(a < b)"

| a < b
|
bool smaller(bool a, bool b) {
	cpp "return false;";
} KeY "(false)"

| a > b
|
bool greater(int a, int b) {
	cpp "return (a > b);";
} KeY "(a > b)"

| a > b
|
bool greater(bool a, bool b) {
	cpp "return false;";
} KeY "(false)"

| a = b
|
bool equal(int a, int b) {
	cpp "return (a == b);";
} KeY "(a = b)"

| a = b
|
bool equal(bool a, bool b) {
	cpp "return (a == b);";
} KeY "(a <-> b)"

| a + b
|
int add(int a, int b) {
	cpp "return (a + b);";
} KeY "(a + b)"

| a - b
|
int subtract(int a, int b) {
	cpp "return (a - b);";
} KeY "(a - b)"

| a * b
|
int multiply(int a, int b) {
	cpp "return (a * b);";
} KeY "(a * b)"

| a / b
|
int divide(int a, int b)
pre  { @ b <> 0; }
body { cpp "return floor(double(a) / double(b));"; }
KeY  "(\\if (b < 0) \\then ((-a) / (-b)) \\else (a / b))"

| a mod b
|
int modulo(int a, int b) {
	cpp "return a - b * floor(double(a) / double((b == 0) + b))";
} KeY "(a - b*(\\if (b < 0) \\then ((-a) / (-b)) \\else (a / b)))"

| ! a
|
bool not(bool a) {
	cpp "return !a;";
} KeY "(!a)"

| - a
|
int negative(int a) {
	cpp "return -a;";
} KeY "(-a)"

| + a
|
int positive(int a) {
	cpp "return a;";
} KeY "(a)"

| # a
|
int count?(T)(T[] a) {
	cpp "return a.size();";
} KeY "(a.length)"

| a[i]
|
T subscript?(T)(T[] a, int i)
pre { @ 1 <= i <= #a; }
body {
	cpp "return a[i];";
} KeY "(a[i])"

void write(int v) {
	cpp "std::cout << v << endl;";
}

void write(bool v) {
	cpp "std::cout << (v ? \"true\" : \"false\") << endl;";
}

int abs(int v) {
	if (v < 0) v <- -v;
	result <- v;
} KeY "(\\if (v < 0) \\then (-v) \\else (v))"
